k:, A:((:( List)  (:  ( List))) List), y:( List). q-sat-constraints(k;A;y)   

latex

Definitions	False, A, P  Q, x. t(x), A  B, let x,y,z = a in t(x;y;z), A c B, q-sat-constraints(k;A;y), , t  T, x:A. B(x), x(s), , S  T
Lemmas	l member wf, qless wf, qle wf, nat wf, int inc rationals, select? wf, q-linear wf, eq int wf, ifthenelse wf, l all wf2, rationals wf, length wf1